(declare-fun v0 () Bool)
(declare-fun v1 () Bool)
(declare-fun v2 () Bool)
(declare-fun v3 () Bool)
(declare-fun v4 () Bool)
(declare-fun v5 () Bool)
(declare-fun v6 () Bool)
(declare-fun v7 () Bool)
(declare-fun v8 () Bool)
(declare-fun v9 () Bool)
(declare-fun v10 () Bool)
(declare-fun i0 () Int)
(declare-fun i3 () Int)
(declare-fun str0 () String)
(declare-fun str1 () String)
(declare-fun str2 () String)
(declare-fun str3 () String)
(declare-fun str4 () String)
(declare-fun str5 () String)
(assert (or v6 (not v9) (not v10) v9 (not v6) v6 (not v8) v7 (not v8) v0 (not v10)))
(push)
(check-sat)
(pop)
(push)
(assert (or (= i3 (- i3 67 67)) v9))
(declare-fun i4 () Int)
(assert (or v0 (not (str.in_re str1 re.all)) (not v3) (not v9) (not (= (- i3 67 67) (- (str.len str5) 91))) v5 (not (= (- i3 67 67) (- (str.len str5) 91))) (not (= 91 i3)) (= (- i3 67 67) (- (str.len str5) 91)) v9 (not (str.in_re str2 (str.to_re "9tgDpjZbJHxREsxrL"))) v7 (not v10)))
(assert (or v4 (not v5)))
(push)
(assert (or (>= (str.len str1) (- 91) (- (- (str.len str5) 91) (- (- i3 67 67) i3) (str.len (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))) (str.len (str.replace_re (str.++ str0 (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))))) (str.to_re str0) (str.++ str3 str1))))) (not v1) (not v1) (not (str.prefixof (str.replace_re_all str2 re.allchar str2) str3)) (distinct (- (- i3 67 67) i3) (* (str.len str1) 91 i3)) v7 (< 67 (- (- i0 (* (str.len str1) 91 i3) i0 91) (- 91)) (- i3 67 67)) (not (= (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))))) (str.++ str0 (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))))) (str.++ str3 str2))) (= 91 i3) (= i3 (str.len (str.substr str4 (- (str.len str5) 91) (- (- i3 67 67) i3))) i3 (str.len (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))) (- 91) (- i3 67 67))))
(push)
(assert (or (str.in_re (str.++ str1 (str.++ (str.substr str2 i3 (str.to_int (str.++ str3 str2))) str3) (str.substr (str.++ str0 (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))))) (str.len str1) (* (str.len str1) 91 i3)) (str.replace_re_all str2 re.allchar str2)) re.all) (not (str.in_re (str.++ str1 (str.++ (str.substr str2 i3 (str.to_int (str.++ str3 str2))) str3) (str.substr (str.++ str0 (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))))) (str.len str1) (* (str.len str1) 91 i3)) (str.replace_re_all str2 re.allchar str2)) re.all)) (not (= (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))))) (str.++ str0 (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))))) (str.++ str3 str2)))))
(assert (or (>= (str.len (str.substr str4 (- (str.len str5) 91) (- (- i3 67 67) i3))) 67) (not (str.in_re (str.replace_re_all str2 re.allchar str2) re.none)) (not (distinct (- i0 (str.len (str.substr str4 (- (str.len str5) 91) (- (- i3 67 67) i3))) (- (- i3 67 67) i3)) (- 91))) (= 91 i3) (distinct (str.substr (str.replace_re str1 re.none (str.substr (str.substr str2 (- (str.len str5) 91) (str.to_int "K4")) (* (+ i3 67 91 (str.len (str.substr str4 (- (str.len str5) 91) (- (- i3 67 67) i3))) (str.len str1)) (+ 91 91) (+ 91 91) 67 (+ 91 91)) i3)) 67 (str.to_int (str.++ (str.++ (str.replace_re (str.++ str0 (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))))) (str.to_re str0) (str.++ str3 str1)) (str.substr str2 (- (str.len str5) 91) (str.to_int "K4"))) (str.replace_re_all str2 re.allchar str2)))) (str.substr (str.substr (str.++ str0 (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))))) i3 (str.len (str.substr str4 (- (str.len str5) 91) (- (- i3 67 67) i3)))) (str.len (str.substr str4 (- (str.len str5) 91) (- (- i3 67 67) i3))) (str.to_int "K4")) (str.replace_re (str.++ str0 (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))))) (str.to_re str0) (str.++ str3 str1))) (str.contains str4 (str.++ (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) (str.len str1) (str.len str5)) (str.++ str3 "1cguWC6Kd") (str.++ (str.substr str2 i3 (str.to_int (str.++ str3 str2))) str3) (str.from_int (abs (* (str.len str1) 91 i3))) (str.substr (str.replace_re str1 re.none (str.substr (str.substr str2 (- (str.len str5) 91) (str.to_int "K4")) (* (+ i3 67 91 (str.len (str.substr str4 (- (str.len str5) 91) (- (- i3 67 67) i3))) (str.len str1)) (+ 91 91) (+ 91 91) 67 (+ 91 91)) i3)) (str.len (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))))) (str.to_int (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) (str.len str1) (str.len str5)))))) (distinct (- (str.len str5) 91) (- i3 67 67)) (not (distinct (- i0 (str.len (str.substr str4 (- (str.len str5) 91) (- (- i3 67 67) i3))) (- (- i3 67 67) i3)) (- 91))) (not v6) (str.contains str4 (str.++ (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) (str.len str1) (str.len str5)) (str.++ str3 "1cguWC6Kd") (str.++ (str.substr str2 i3 (str.to_int (str.++ str3 str2))) str3) (str.from_int (abs (* (str.len str1) 91 i3))) (str.substr (str.replace_re str1 re.none (str.substr (str.substr str2 (- (str.len str5) 91) (str.to_int "K4")) (* (+ i3 67 91 (str.len (str.substr str4 (- (str.len str5) 91) (- (- i3 67 67) i3))) (str.len str1)) (+ 91 91) (+ 91 91) 67 (+ 91 91)) i3)) (str.len (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))))) (str.to_int (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) (str.len str1) (str.len str5)))))) (not v9) (not (str.prefixof (str.replace_re_all str2 re.allchar str2) str3))))
(pop)
(assert (or (= (str.++ (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) (str.substr (str.++ str0 (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))))) (str.len str1) (* (str.len str1) 91 i3))) (str.substr (str.++ str0 (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))))) i3 (str.len (str.substr str4 (- (str.len str5) 91) (- (- i3 67 67) i3)))) (str.replace_re str1 re.none (str.substr (str.substr str2 (- (str.len str5) 91) (str.to_int "K4")) (* (+ i3 67 91 (str.len (str.substr str4 (- (str.len str5) 91) (- (- i3 67 67) i3))) (str.len str1)) (+ 91 91) (+ 91 91) 67 (+ 91 91)) i3)) (str.substr str1 (- (- 91)) (- (- 91)))) (= (str.substr (str.replace_re str1 re.none (str.substr (str.substr str2 (- (str.len str5) 91) (str.to_int "K4")) (* (+ i3 67 91 (str.len (str.substr str4 (- (str.len str5) 91) (- (- i3 67 67) i3))) (str.len str1)) (+ 91 91) (+ 91 91) 67 (+ 91 91)) i3)) 67 (str.to_int (str.++ (str.++ (str.replace_re (str.++ str0 (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))))) (str.to_re str0) (str.++ str3 str1)) (str.substr str2 (- (str.len str5) 91) (str.to_int "K4"))) (str.replace_re_all str2 re.allchar str2)))) (str.++ (str.substr str2 i3 (str.to_int (str.++ str3 str2))) str3) (str.replace_re str2 (str.to_re "") str1)) (not (distinct str2 str0)) (not (>= (str.len str1) (- 91) (- (- (str.len str5) 91) (- (- i3 67 67) i3) (str.len (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))) (str.len (str.replace_re (str.++ str0 (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))))) (str.to_re str0) (str.++ str3 str1)))))) (not (< 67 (- (- i0 (* (str.len str1) 91 i3) i0 91) (- 91)) (- i3 67 67))) (not (< 67 (- (- i0 (* (str.len str1) 91 i3) i0 91) (- 91)) (- i3 67 67))) (not v3) v2 (not (>= i3 i3 67 (- (str.len str5) 91))) v8 (str.suffixof (str.replace_re str1 re.all str3) (str.++ (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) (str.len str1) (str.len str5)) (str.++ str3 "1cguWC6Kd") (str.++ (str.substr str2 i3 (str.to_int (str.++ str3 str2))) str3) (str.from_int (abs (* (str.len str1) 91 i3))) (str.substr (str.replace_re str1 re.none (str.substr (str.substr str2 (- (str.len str5) 91) (str.to_int "K4")) (* (+ i3 67 91 (str.len (str.substr str4 (- (str.len str5) 91) (- (- i3 67 67) i3))) (str.len str1)) (+ 91 91) (+ 91 91) 67 (+ 91 91)) i3)) (str.len (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))))) (str.to_int (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) (str.len str1) (str.len str5))))))))
(assert (or (distinct (- (str.len str5) 91) (- i3 67 67)) (str.in_re (str.++ (str.++ str3 "1cguWC6Kd") (str.replace_re str1 re.all str3)) re.allchar)))
(assert (or (str.suffixof (str.replace_re str1 re.all str3) (str.++ (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) (str.len str1) (str.len str5)) (str.++ str3 "1cguWC6Kd") (str.++ (str.substr str2 i3 (str.to_int (str.++ str3 str2))) str3) (str.from_int (abs (* (str.len str1) 91 i3))) (str.substr (str.replace_re str1 re.none (str.substr (str.substr str2 (- (str.len str5) 91) (str.to_int "K4")) (* (+ i3 67 91 (str.len (str.substr str4 (- (str.len str5) 91) (- (- i3 67 67) i3))) (str.len str1)) (+ 91 91) (+ 91 91) 67 (+ 91 91)) i3)) (str.len (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))))) (str.to_int (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) (str.len str1) (str.len str5)))))) (not (> (* (str.len str1) 91 i3) (str.len str1))) (str.in_re (str.replace_re_all str2 re.allchar str2) re.none) (not (str.in_re (str.++ (str.++ str3 "1cguWC6Kd") (str.replace_re str1 re.all str3)) re.allchar))))
(push)
(assert (or (distinct (- (str.len str5) 91) (- i3 67 67)) (not (distinct str2 str0)) (not v0) (not (distinct (- i3 67 67) (- i0 (str.len (str.substr str4 (- (str.len str5) 91) (- (- i3 67 67) i3))) (- (- i3 67 67) i3)))) (not (= (str.++ str3 str1) (str.substr (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))))) (- (- i3 67 67) i3) (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))))) str3)) (not (= (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))))) (str.++ str0 (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))))) (str.++ str3 str2))) (str.suffixof (str.replace_re str1 re.all str3) (str.++ (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) (str.len str1) (str.len str5)) (str.++ str3 "1cguWC6Kd") (str.++ (str.substr str2 i3 (str.to_int (str.++ str3 str2))) str3) (str.from_int (abs (* (str.len str1) 91 i3))) (str.substr (str.replace_re str1 re.none (str.substr (str.substr str2 (- (str.len str5) 91) (str.to_int "K4")) (* (+ i3 67 91 (str.len (str.substr str4 (- (str.len str5) 91) (- (- i3 67 67) i3))) (str.len str1)) (+ 91 91) (+ 91 91) 67 (+ 91 91)) i3)) (str.len (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))))) (str.to_int (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) (str.len str1) (str.len str5)))))) (< i0 (- i3 67 67)) (distinct (- (str.len str5) 91) (- i3 67 67)) (not (= (str.++ str3 str1) (str.substr (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))))) (- (- i3 67 67) i3) (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))))) str3)) (not (distinct (- (str.len str5) 91) (- i0 (str.len (str.substr str4 (- (str.len str5) 91) (- (- i3 67 67) i3))) (- (- i3 67 67) i3)) (+ i3 67 91 (str.len (str.substr str4 (- (str.len str5) 91) (- (- i3 67 67) i3))) (str.len str1)) (+ 91 91))) (str.in_re (str.replace_re_all str2 re.allchar str2) re.none)))
(check-sat)
(assert (or (= (str.len str5) (- (- (str.len str5) 91) (- (- i3 67 67) i3) (str.len (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))) (str.len (str.replace_re (str.++ str0 (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))))) (str.to_re str0) (str.++ str3 str1))))) (= (str.++ str3 str1) (str.substr (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))))) (- (- i3 67 67) i3) (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))))) str3) (not (str.in_re (str.++ str1 (str.++ (str.substr str2 i3 (str.to_int (str.++ str3 str2))) str3) (str.substr (str.++ str0 (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))))) (str.len str1) (* (str.len str1) 91 i3)) (str.replace_re_all str2 re.allchar str2)) re.all))))
(assert (or (distinct 91 i0) v8 (> (str.len (str.++ str0 (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))))))) (abs (* (str.len str1) 91 i3))) (not (>= (str.len (str.substr str4 (- (str.len str5) 91) (- (- i3 67 67) i3))) 67)) (not (= (str.substr (str.replace_re str1 re.none (str.substr (str.substr str2 (- (str.len str5) 91) (str.to_int "K4")) (* (+ i3 67 91 (str.len (str.substr str4 (- (str.len str5) 91) (- (- i3 67 67) i3))) (str.len str1)) (+ 91 91) (+ 91 91) 67 (+ 91 91)) i3)) 67 (str.to_int (str.++ (str.++ (str.replace_re (str.++ str0 (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))))) (str.to_re str0) (str.++ str3 str1)) (str.substr str2 (- (str.len str5) 91) (str.to_int "K4"))) (str.replace_re_all str2 re.allchar str2)))) (str.++ (str.substr str2 i3 (str.to_int (str.++ str3 str2))) str3) (str.replace_re str2 (str.to_re "") str1))) (not v6) (not (distinct (str.substr (str.replace_re str1 re.none (str.substr (str.substr str2 (- (str.len str5) 91) (str.to_int "K4")) (* (+ i3 67 91 (str.len (str.substr str4 (- (str.len str5) 91) (- (- i3 67 67) i3))) (str.len str1)) (+ 91 91) (+ 91 91) 67 (+ 91 91)) i3)) 67 (str.to_int (str.++ (str.++ (str.replace_re (str.++ str0 (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))))) (str.to_re str0) (str.++ str3 str1)) (str.substr str2 (- (str.len str5) 91) (str.to_int "K4"))) (str.replace_re_all str2 re.allchar str2)))) (str.substr (str.substr (str.++ str0 (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))))) i3 (str.len (str.substr str4 (- (str.len str5) 91) (- (- i3 67 67) i3)))) (str.len (str.substr str4 (- (str.len str5) 91) (- (- i3 67 67) i3))) (str.to_int "K4")) (str.replace_re (str.++ str0 (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))))) (str.to_re str0) (str.++ str3 str1)))) (not v8) (not (distinct str2 str0)) (str.suffixof (str.replace_re str1 re.all str3) (str.++ (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) (str.len str1) (str.len str5)) (str.++ str3 "1cguWC6Kd") (str.++ (str.substr str2 i3 (str.to_int (str.++ str3 str2))) str3) (str.from_int (abs (* (str.len str1) 91 i3))) (str.substr (str.replace_re str1 re.none (str.substr (str.substr str2 (- (str.len str5) 91) (str.to_int "K4")) (* (+ i3 67 91 (str.len (str.substr str4 (- (str.len str5) 91) (- (- i3 67 67) i3))) (str.len str1)) (+ 91 91) (+ 91 91) 67 (+ 91 91)) i3)) (str.len (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))))) (str.to_int (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) (str.len str1) (str.len str5)))))) v3 (not (str.in_re (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) (str.len str1) (str.len str5)) re.allchar)) (not (str.in_re (str.replace_re_all str2 re.allchar str2) re.none))))
(push)
(assert (or (str.prefixof (str.replace_re_all str2 re.allchar str2) str3) (str.prefixof str4 str5) (not (< i0 (- i3 67 67))) (not (distinct (str.len (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))) i3 (- i0 (str.len (str.substr str4 (- (str.len str5) 91) (- (- i3 67 67) i3))) (- (- i3 67 67) i3)) (- i3 67 67) (- 91))) (not (str.in_re str2 re.all)) (> (- (str.len (str.substr str4 (- (str.len str5) 91) (- (- i3 67 67) i3))) (str.len str1) (- 91 (str.len str5) (str.len (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))))) (str.len str1)) (- i0 (str.len (str.substr str4 (- (str.len str5) 91) (- (- i3 67 67) i3))) (- (- i3 67 67) i3))) (- 91)) (not (str.contains (str.++ (str.++ (str.++ str3 "1cguWC6Kd") (str.replace_re str1 re.all str3)) "K4") (str.replace_re (str.++ (str.substr (str.substr (str.++ str0 (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))))) (str.len str1) (* (str.len str1) 91 i3)) (str.len str1) (- 91 (str.len str5) (str.len (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))))) (str.len str1))) "K4") re.none (str.++ str1 (str.++ (str.substr str2 i3 (str.to_int (str.++ str3 str2))) str3) (str.substr (str.++ str0 (str.substr (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2)))) 91 (str.to_int (str.replace_re_all str3 re.allchar (str.substr str2 i3 (str.to_int (str.++ str3 str2))))))) (str.len str1) (* (str.len str1) 91 i3)) (str.replace_re_all str2 re.allchar str2)))))))
(pop)
(check-sat)
